e receives || a == (isrcv(e))  val(e):valtype(e)||a 

latex

---

clarification:

es-rcv-atom(es;e;a)
== (es-isrcv(es; e))  free-from-atom{1}(es-valtype(es; e);es-val(es; e);a) 

latex

Definitions	P  Q, b, isrcv(e), x:T||a, valtype(e), val(e)
FDL editor aliases	es-rcv-atom